Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems
Identifieur interne : 005521 ( Main/Exploration ); précédent : 005520; suivant : 005522Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems
Auteurs : Frédéric Blanqui Inria [France] ; Colin Riba Inpl [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
English descriptors
Abstract
Abstract: In a previous work, the first author extended to higher-order rewriting and dependent types the use of size annotations in types, a termination proof technique called type or size based termination and initially developed for ML-like programs. Here, we go one step further by considering conditional rewriting and explicit quantifications and constraints on size annotations. This allows to describe more precisely how the size of the output of a function depends on the size of its inputs. Hence, we can check the termination of more functions. We first give a general type-checking algorithm based on constraint solving. Then, we give a termination criterion with constraints in Presburger arithmetic. To our knowledge, this is the first termination criterion for higher-order conditional rewriting taking into account the conditions in termination.
Url:
DOI: 10.1007/11916277_8
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 002310
- to stream Istex, to step Curation: 002279
- to stream Istex, to step Checkpoint: 001374
- to stream Hal, to step Corpus: 001616
- to stream Hal, to step Curation: 001616
- to stream Hal, to step Checkpoint: 003E58
- to stream Main, to step Merge: 005667
- to stream Main, to step Curation: 005521
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems</title><author><name sortKey=" Inria, Frederic Blanqui" sort=" Inria, Frederic Blanqui" uniqKey=" Inria F" first="Frédéric Blanqui" last=" Inria">Frédéric Blanqui Inria</name></author><author><name sortKey=" Inpl, Colin Riba" sort=" Inpl, Colin Riba" uniqKey=" Inpl C" first="Colin Riba" last=" Inpl">Colin Riba Inpl</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:96301D2389FBC38D063E62ED1F16846C4CCE5ED3</idno><date when="2006" year="2006">2006</date><idno type="doi">10.1007/11916277_8</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-JFTJ83LR-S/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">002310</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002310</idno><idno type="wicri:Area/Istex/Curation">002279</idno><idno type="wicri:Area/Istex/Checkpoint">001374</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001374</idno><idno type="wicri:doubleKey">0302-9743:2006: Inria F:combining:typing:and</idno><idno type="wicri:source">HAL</idno><idno type="RBID">Hal:inria-00084837</idno><idno type="url">https://hal.inria.fr/inria-00084837</idno><idno type="wicri:Area/Hal/Corpus">001616</idno><idno type="wicri:Area/Hal/Curation">001616</idno><idno type="wicri:Area/Hal/Checkpoint">003E58</idno><idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">003E58</idno><idno type="wicri:Area/Main/Merge">005667</idno><idno type="wicri:Area/Main/Curation">005521</idno><idno type="wicri:Area/Main/Exploration">005521</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems</title><author><name sortKey=" Inria, Frederic Blanqui" sort=" Inria, Frederic Blanqui" uniqKey=" Inria F" first="Frédéric Blanqui" last=" Inria">Frédéric Blanqui Inria</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>LORIA, Campus Scientifique, BP 239, 54506 Cedex, Vandoeuvre-lès-Nancy</wicri:regionArea><placeName><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region><settlement type="city">Vandœuvre-lès-Nancy</settlement><settlement type="city" wicri:auto="agglo">Nancy</settlement></placeName></affiliation></author><author><name sortKey=" Inpl, Colin Riba" sort=" Inpl, Colin Riba" uniqKey=" Inpl C" first="Colin Riba" last=" Inpl">Colin Riba Inpl</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>LORIA, Campus Scientifique, BP 239, 54506 Cedex, Vandoeuvre-lès-Nancy</wicri:regionArea><placeName><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region><settlement type="city">Vandœuvre-lès-Nancy</settlement><settlement type="city" wicri:auto="agglo">Nancy</settlement></placeName></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="mix" xml:lang="en"><term>conditional rewriting</term><term>lambda-calculus</term><term>size constraints</term><term>termination</term><term>typing</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: In a previous work, the first author extended to higher-order rewriting and dependent types the use of size annotations in types, a termination proof technique called type or size based termination and initially developed for ML-like programs. Here, we go one step further by considering conditional rewriting and explicit quantifications and constraints on size annotations. This allows to describe more precisely how the size of the output of a function depends on the size of its inputs. Hence, we can check the termination of more functions. We first give a general type-checking algorithm based on constraint solving. Then, we give a termination criterion with constraints in Presburger arithmetic. To our knowledge, this is the first termination criterion for higher-order conditional rewriting taking into account the conditions in termination.</div></front></TEI><affiliations><list><country><li>France</li></country><region><li>Grand Est</li><li>Lorraine (région)</li></region><settlement><li>Nancy</li><li>Vandœuvre-lès-Nancy</li></settlement></list><tree><country name="France"><region name="Grand Est"><name sortKey=" Inria, Frederic Blanqui" sort=" Inria, Frederic Blanqui" uniqKey=" Inria F" first="Frédéric Blanqui" last=" Inria">Frédéric Blanqui Inria</name></region><name sortKey=" Inpl, Colin Riba" sort=" Inpl, Colin Riba" uniqKey=" Inpl C" first="Colin Riba" last=" Inpl">Colin Riba Inpl</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 005521 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 005521 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:96301D2389FBC38D063E62ED1F16846C4CCE5ED3
|texte= Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems
}}
| This area was generated with Dilib version V0.6.33. |  |